Inference at * 2 2 1 1 1 
Iof proof for Lemma before-adjacent:



1. T : Type
2. T List
3. u : T
4. v : T List
5. x, y:T.
5. no_repeats(T;v)  adjacent(T;v;x;y)  (z:T. z before y  v  (z before x  v  (z = x)))
6. x : T
7. y : T
8. no_repeats(T;v)
9. (u  v)
10. 0 < ||v||
11. adjacent(T;v;x;y)
12. z : T
13. z = u
14. (y  v)
15. z:T. z before y  v  (z before x  v  (z = x))
  z before x  [u / v] 

latex

 by ((((RWO "cons_before" (0)) 
THENM (OrLeft))) 
TCollapseTHEN (Auto)) 

latex

TC1: 

TC1:   (x  v)
TC.

Definitions	P  Q, P  Q, P  Q, P  Q, P & Q, x:A  B(x), ||as||, , (x  l), adjacent(T;L;x;y), a < b, A, no_repeats(T;l), type List, Type, x before y  l, x:A. B(x), x:AB(x), t  T, s = t
Lemmas	cons before, l member wf, l before wf